28.9 KB · ⇊ 8 parts · ⤓ Micron 28.9 KB · ⤓ HTML 168.8 KB

top

Il mwcglambda calcolo o mwcwλ-calcolo è un mwdasistema formale definito nel 1936 dal matematico mwdqAlonzo Church, sviluppato per analizzare formalmente le mwdgfunzioni e il loro mwdwcalcolo. Le prime sono espresse per mezzo di un mwealinguaggio formale, che stabilisce quali siano le regole per formare un termine, il secondo con un sistema di mweqriscrittura, che definisce come i termini possano essere ridotti e semplificati.

• Descrizione

• Termini

• Variabili

• Regole di riscrittura

• Sostituzione

• Alfa conversione

• Beta riduzione

• Eta conversione

• Termini equivalenti

• Codifiche

• Numerazione

• Operazioni aritmetiche

• Logica di Boole

• Operazioni logiche

• Forme normali

• Note

• Bibliografia

• Voci correlate

• Altri progetti

• Collegamenti esterni

La combinazione di semplicità ed espressività ha reso il lambda calcolo uno strumento frequente in diversi campi scientifici:

• Nell'ambito della mwfwmatematica e nell'mwgainformatica, in particolare nella mwgqteoria della calcolabilità fu sviluppato per lo studio delle mwggfunzioni ricorsive come effettivamente calcolabili.

• Nell'mwhainformatica e nella mwhqteoria dei linguaggi di programmazione è il principale prototipo dei mwhglinguaggi di programmazione di tipo mwhwfunzionale e della mwiaricorsione.

• Nella mwigteoria della dimostrazione, il lambda calcolo tipato è uno dei più usati sistemi formali per la rappresentazione delle dimostrazioni, grazie alla corrispondenza Curry-Howard che mette in relazione dimostrazioni con termini e tipi con formule logiche.

• Nella mwjgsemantica modellistica (branca della mwjwlinguistica) il lambda calcolo è il formalismo impiegato per la descrizione della composizione del mwkasignificato all'interno di una mwkqfrase.

Si definisce mwlatermine del lambda calcolo o, più brevemente, mwlqlambda termine o mwlglambda espressione qualunque stringa ben formata a partire dalla seguente mwlwgrammatica, in mwmaforma Backus-Naur:

mwmg T ::= V | λ λ V . T | ( T T ) {\displaystyle T\quad ::=\quad V\quad |\quad \lambda V.T\quad |\quad (T\quad T)}

dove la metavariabile mwna V {\displaystyle V} denota una variabile appartenente a un insieme mwnqinfinito mwngnumerabile di variabili.

Parafrasando la definizione formale, un lambda termine può essere, rispettivamente, un nome di variabile, lmwoa'astrazione di un termine rispetto ad una variabile, o lmwoq'applicazione di un termine come argomento (o parametro attuale) di un altro.

Dato un generico lambda termine mwpa M {\displaystyle M} , si definisce mwpq V a r ( M ) {\displaystyle \mathrm {Var} (M)} l'insieme che contiene tutte le variabili menzionate in mwpg M {\displaystyle M} . Tra queste si distinguono due partizioni: l'insieme delle mwqavariabili libere, scritto mwqq L i b e r e ( M ) {\displaystyle \mathrm {Libere} (M)} , e l'insieme delle variabili legate, indicate con mwqg L e g a t e ( M ) {\displaystyle \mathrm {Legate} (M)} . L'insieme delle variabili libere è definito ricorsivamente come segue:

1. mwrq L i b e r e ( x ) = { x } {\displaystyle \mathrm {Libere} (x)=\{x\}} ;

2. mwrw L i b e r e ( λ λ x . M ) = L i b e r e ( M ) ∖ ∖ { x } {\displaystyle \mathrm {Libere} (\lambda x.M)=\mathrm {Libere} (M)\setminus \{x\}} ;

3. mwsq L i b e r e ( M N ) = L i b e r e ( M ) ∪ ∪ L i b e r e ( N ) {\displaystyle \mathrm {Libere} (MN)=\mathrm {Libere} (M)\cup \mathrm {Libere} (N)} .

L'insieme delle variabili legate è quindi ottenibile per differenza:

mwtq L e g a t e ( M ) = V a r ( M ) ∖ ∖ L i b e r e ( M ) {\displaystyle \mathrm {Legate} (M)=Var(M)\setminus \mathrm {Libere} (M)} .

Il punto 2 della definizione implica che il costrutto sintattico dell'astrazione è un legatore di variabile: se mwtw x ∈ ∈ Libere ( M ) {\displaystyle x\in {\textrm {Libere}}(M)} , allora mwua x ∈ ∈ Legate ( λ λ x . M ) {\displaystyle x\in {\textrm {Legate}}(\lambda x.M)} .

Un mwugnome di variabile si dice mwuwfresco, relativamente ad un termine, se esso non è compreso tra i nomi di variabile di quello stesso termine.

Alcuni esempi che si ottengono semplicemente applicando le definizioni date sopra:

mwvw Var ( λ λ z . λ λ x . ( x y ) ) = { z , x , y } {\displaystyle {\textrm {Var}}(\lambda z.\lambda x.(xy))=\{z,x,y\}} ;

mwwq Libere ( λ λ z . λ λ x . ( x y ) ) = { y } {\displaystyle {\textrm {Libere}}(\lambda z.\lambda x.(xy))=\{y\}} ;

mwww Legate ( λ λ z . λ λ x . ( x y ) ) = { x , z } {\displaystyle {\textrm {Legate}}(\lambda z.\lambda x.(xy))=\{x,z\}} ;

Una sostituzione è il rimpiazzo di tutte le occorrenze di un sotto-termine con un altro, all'interno di un terzo termine che rappresenta il contesto della sostituzione stessa. Si indica con mwxw M [ N / v ] {\displaystyle M[N/v]} la sostituzione del termine mwya N {\displaystyle N} al posto di mwyq v {\displaystyle v} all'interno del termine mwyg M {\displaystyle M} : ogni occorrenza libera della variabile mwyw v {\displaystyle v} in mwza M {\displaystyle M} è sostituita da mwzq N {\displaystyle N} . Un semplice esempio di sostituzione è il seguente:

mwaa ( z x ) [ λ λ x . x / z ] ≡ ≡ ( ( λ λ x . x ) x ) {\displaystyle (zx)[\lambda x.x/z]\equiv ((\lambda x.x)x)} .

Una definizione ricorsiva dell'algoritmo di sostituzione è la successiva:

1. mwba x [ N / x ] ≡ ≡ N {\displaystyle x[N/x]\equiv N} ;

2. mwbg y [ N / x ] ≡ ≡ y {\displaystyle y[N/x]\equiv y} , se mwbw x ≠ ≠ y {\displaystyle x\neq y} ;

3. mwcq ( λ λ y . M ) [ N / y ] ≡ ≡ λ λ y . M {\displaystyle (\lambda y.M)[N/y]\equiv \lambda y.M} ;

4. mwcw ( λ λ y . M ) [ N / x ] ≡ ≡ λ λ y . ( M [ N / x ] ) {\displaystyle (\lambda y.M)[N/x]\equiv \lambda y.(M[N/x])} , se mwda y ≠ ≠ x {\displaystyle y\neq x} e mwdq y ∉ ∉ F V ( N ) {\displaystyle y\notin FV(N)} ;

5. mwdw ( λ λ y . M ) [ N / x ] ≡ ≡ λ λ z . ( M [ z / y ] [ N / x ] ) {\displaystyle (\lambda y.M)[N/x]\equiv \lambda z.(M[z/y][N/x])} , se mwea y ≠ ≠ x {\displaystyle y\neq x} , mweq y ∈ ∈ F V ( N ) {\displaystyle y\in FV(N)} , e mweg z {\displaystyle z} è un nome fresco;

6. mwfa ( M 1 M 2 ) [ N / x ] ≡ ≡ ( M 1 [ N / x ] ) ( M 2 [ N / x ] ) {\displaystyle (M_{1}M_{2})[N/x]\equiv (M_{1}[N/x])(M_{2}[N/x])} .

Alcuni esempi di sostituzione:

mwga ( z x ) [ ( λ λ x . x ) / z ] ≡ ≡ ( ( λ λ x . x ) x ) {\displaystyle (zx)[(\lambda x.x)/z]\equiv ((\lambda x.x)x)} ;

mwgg ( λ λ z . ( z x ) ) [ ( λ λ x . x ) / z ] ≡ ≡ ( λ λ z . ( z x ) ) {\displaystyle (\lambda z.(zx))[(\lambda x.x)/z]\equiv (\lambda z.(zx))} ;

mwha ( λ λ z . ( z x ) ) [ ( z x ) / x ] ≡ ≡ λ λ w . ( ( z x ) [ w / z ] [ ( z x ) / x ] ) ≡ ≡ λ λ w . ( ( w x ) [ ( z x ) / x ] ) ≡ ≡ λ λ w . w ( z x ) {\displaystyle (\lambda z.(zx))[(zx)/x]\equiv \lambda w.((zx)[w/z][(zx)/x])\equiv \lambda w.((wx)[(zx)/x])\equiv \lambda w.w(zx)} , dove mwhq w {\displaystyle w} è un nome fresco.

I mwhwcontrolli di occorrenza al punto 4 e 5, sono necessari per evitare un fenomeno sgradito chiamato mwiacattura di variabile. Senza tali controlli, l'operazione di sostituzione porterebbe una variabile mwiqlibera di un termine, a diventare mwiglegata per effetto della sostituzione stessa, il che risulta essere anche intuitivamente scorretto.

mwjq λ λ x . M → → α α λ λ y . ( M [ y / x ] ) {\displaystyle \lambda x.M\rightarrow _{\alpha }\lambda y.(M[y/x])} .

Lmwjw'alfa conversione si applica ai termini che sono astrazioni. Data un'astrazione, è possibile riscriverla sostituendo la variabile astratta (mwka x {\displaystyle x} ) con un'altra (mwkq y {\displaystyle y} ), a patto che, nell'intero sotto-termine, al posto di ogni occorrenza della prima, si scriva la seconda.

La regola di alfa conversione non si occupa di fare alcuna distinzione fra occorrenze mwkwlibere o mwlalegate delle variabili, dato che l'operazione di sostituzione si occupa già di fare ciò. Alcuni esempi di alfa conversione:

mwlw λ λ x . ( x y ) → → α α λ λ z . ( z y ) {\displaystyle \lambda x.(xy)\rightarrow _{\alpha }\lambda z.(zy)}

mwmq λ λ x . ( x ( λ λ z . ( z w ) ) ) → → α α λ λ z . ( z ( λ λ z . ( z w ) ) ) {\displaystyle \lambda x.(x(\lambda z.(zw)))\rightarrow _{\alpha }\lambda z.(z(\lambda z.(zw)))}

La mwnabeta riduzione è la più importante regola di riscrittura del lambda calcolo, visto che implementa il passo di computazione. La sua prescrizione è definita come segue, dove l'eventuale contesto presente è omesso:

mwnw ( λ λ x . M ) N → → β β M [ N / x ] {\displaystyle (\lambda x.M)N\rightarrow _{\beta }M[N/x]} .

(Sostituire N, alle occorrenze delle variabili legate, in M)

La regola ha come oggetto un'applicazione di una lambda astrazione nella forma mwog λ λ x . M {\displaystyle \lambda x.M} su un secondo termine mwow N {\displaystyle N} . La configurazione sintattica riducibile è appunto chiamata mwparedex, contrazione della inglese "red-ucible ex-pression", a sua volta raramente mwpqricalcato in italiano come "redesso", il suo risultato è chiamato ridotto.

Proseguendo l'analogia con i linguaggi di programmazione, la regola riguarda una funzione applicata ad un argomento. Essa corrisponde pertanto ad un passo di calcolo, che restituisce il corpo della funzione mwpw M {\displaystyle M} dove il mwqaparametro attuale (effettivo) mwqq N {\displaystyle N} viene sostituito al mwqgparametro formale mwqw x {\displaystyle x} della funzione. In questo contesto dunque la sostituzione rappresenta proprio il mwrapassaggio del parametro.

Alcuni esempi di beta riduzione sono:

mwsa ( λ λ x . ( x x ) ) ( λ λ y . y ) → → β β ( λ λ y . y ) ( λ λ y . y ) → → β β λ λ y . y {\displaystyle (\lambda x.(xx))(\lambda y.y)\rightarrow _{\beta }(\lambda y.y)(\lambda y.y)\rightarrow _{\beta }\lambda y.y}

mwsg ( λ λ x . λ λ y . ( x y ) ) ( λ λ x . ( x x ) ) ( λ λ y . y ) → → β β ( λ λ x . ( x x ) ) ( λ λ y . y ) → → β β ⋯ ⋯ → → β β λ λ y . y {\displaystyle (\lambda x.\lambda y.(xy))(\lambda x.(xx))(\lambda y.y)\rightarrow _{\beta }(\lambda x.(xx))(\lambda y.y)\rightarrow _{\beta }\dots \rightarrow _{\beta }\lambda y.y}

mwtq λ λ x . ( M x ) → → η η M {\displaystyle \lambda x.(Mx)\rightarrow _{\eta }M} , se mwtg x ∉ ∉ F V ( M ) {\displaystyle x\notin FV(M)} .

Intuitivamente, l'importanza di questa regola risiede nel fatto che consente di dichiarare mwuaidentici due lambda termini sulla base del principio che se essi si mwuqcomportano allo stesso modo (una volta applicati ad un parametro) essi devono quindi essere considerati, per l'appunto, identici.

Dire che mwuw λ λ x . ( M x ) {\displaystyle \lambda x.(Mx)} e mwva M {\displaystyle M} si comportano allo stesso modo, equivale a dire che per ogni mwvq N {\displaystyle N} : mwvg ( λ λ x . ( M x ) ) N → → β β ( M x ) [ N / x ] ≡ ≡ ( M N ) {\displaystyle (\lambda x.(Mx))N\rightarrow _{\beta }(Mx)[N/x]\equiv (MN)} . In altre parole mwvwla eta-conversione assiomatizza la dimostrabilità dell'uguaglianza nel mwwq λ λ {\displaystyle \lambda } -calcolo estensionalecite-ref-1[1].

Le regole di conversione possono essere estese a vere e proprie relazioni di equivalenza, assumendo di poter riscrivere nel senso delle frecce appena definite (da sinistra verso destra) e che valgano anche le riscritture nella direzione opposta (da destra verso sinistra, quindi). Formalmente, si applicano le seguenti relazioni:

• mwyg λ λ x . M ⇔ ⇔ α α λ λ y . ( M [ y / x ] ) {\displaystyle \lambda x.M\Leftrightarrow _{\alpha }\lambda y.(M[y/x])} ,

• mwza λ λ x . ( M x ) ⇔ ⇔ η η M {\displaystyle \lambda x.(Mx)\Leftrightarrow _{\eta }M} , se mwzq x ∉ ∉ F V ( M ) {\displaystyle x\notin FV(M)} .

Le due doppie implicazioni sono chiamate, rispettivamente, alfa-equivalenza e eta-equivalenza. Due termini mwzwt ed mw0as si dicono alfa-eta-equivalenti quando è soddifatta la relazione:

mw0g t ⇔ ⇔ x 1 t 1 ⇔ ⇔ x 2 t 2 ⇔ ⇔ x 3 ⋯ ⋯ ⇔ ⇔ x n t n ⇔ ⇔ x n + 1 s ∀ ∀ i . x i ∈ ∈ { α α , η η } {\displaystyle t\Leftrightarrow _{x_{1}}t_{1}\Leftrightarrow _{x_{2}}t_{2}\Leftrightarrow _{x_{3}}\dots \Leftrightarrow _{x_{n}}t_{n}\Leftrightarrow _{x_{n+1}}s\qquad \forall i.x_{i}\in \{\alpha ,\eta \}} .

In altre parole, due termini sono alfa-eta-equivalenti se esiste una catena finita di riscritture che impieghi solo le regole di alfa-equivalenza e di eta-equivalenza.

Attraverso il λ-calcolo sono state formulate diverse codifiche. Alcuni esempi sono la codifica di Church, e quella di Mogensen-Scott. Esistono anche codifiche che usano il lambda calcolo tipato, come il mw2aSistema F.

La numerazione di Church può esprimere l'insieme dei numeri naturali mw2w N {\displaystyle \mathbb {N} } attraverso gli mw3aassiomi di Peano. Ogni numero viene espresso come il successivo del precedente, mentre lo zero è l'unico che non è il successivo di alcun numero.

mw3g n := λ λ s z . s 0 ∘ ∘ s 1 ∘ ∘ ⋯ ⋯ ∘ ∘ s n ( z ) {\displaystyle n:=\lambda sz.s_{0}\circ s_{1}\circ \cdots \circ s_{n}(z)}

Tutti i numeri appartenenti all'insieme dei naturali possono essere espressi analogamente.

mw4q N ∋ ∋ { 0 := λ λ s z . z 1 := λ λ s z . s ( z ) 2 := λ λ s z . s ( s ( z ) ) 3 := λ λ s z . s ( s ( s ( z ) ) ) 4 := λ λ s z . s ( s ( s ( s ( z ) ) ) ) ⋯ ⋯ {\displaystyle \mathbb {N} \ni {\begin{cases}0:=\lambda sz.z\\1:=\lambda sz.s(z)\\2:=\lambda sz.s(s(z))\\3:=\lambda sz.s(s(s(z)))\\4:=\lambda sz.s(s(s(s(z))))\\\cdots \end{cases}}}

Relativamente alla precedente numerazione dei numeri naturali è possibile esprimere alcune computazioni elencate di seguito.

| Funzione | Definizione aritmetica | Definizione secondo Church |

|---|---|---|

| Successore | n + 1 {\displaystyle n+1} | λ w x y . x ( w x y ) {\displaystyle \lambda wxy.x(wxy)} |

| Addizione | x + y {\displaystyle x+y} | λ x y f g . x f ( y f g ) ≡ λ x y . x S U C y {\displaystyle \lambda xyfg.xf(yfg)\equiv \lambda xy.x\;SUC\;y} |

| Moltiplicazione | x ∗ y {\displaystyle x*y} | λ x y f . x ( y f ) {\displaystyle \lambda xyf.x(yf)} |

| Potenza | x y {\displaystyle x^{y}} | λ x y . y ( x ) {\displaystyle \lambda xy.y(x)} |

mwaqg S U C 0 = λ λ w x y . x ( w x y ) ( λ λ s z . z ) = λ λ x y . x ( ( λ λ s z . z ) x y ) = λ λ x y . x ( ( λ λ z . z ) y ) = λ λ x y . x ( y ) = 1 {\displaystyle SUC\;0=\lambda wxy.x(wxy)(\lambda sz.z)=\lambda xy.x((\lambda sz.z)xy)=\lambda xy.x((\lambda z.z)y)=\lambda xy.x(y)=1}

mwaqo 1 A D D 2 = λ λ f g . ( λ λ s z . s ( z ) ) f ( ( λ λ s z . s ( s ( z ) ) ) f g ) = λ λ f g . ( λ λ z . f ( z ) ) ( f ( f ( g ) ) = λ λ f g . f ( f ( f ( g ) ) ) = 3 {\displaystyle 1\;ADD\;2=\lambda fg.(\lambda sz.s(z))f((\lambda sz.s(s(z)))fg)=\lambda fg.(\lambda z.f(z))(f(f(g))=\lambda fg.f(f(f(g)))=3}

mwaqw 1 M U L 3 = ( λ λ s z . s ( z ) ) ( λ λ x y f . x ( y f ) ) ( λ λ s z . s ( s ( s ( z ) ) ) ) = λ λ f . ( λ λ s z . s ( z ) ) ( ( λ λ z . f ( f ( f ( z ) ) ) ) ) = λ λ f . λ λ z . f ( f ( f ( z ) ) ) = 3 {\displaystyle 1\;MUL\;3=(\lambda sz.s(z))(\lambda xyf.x(yf))(\lambda sz.s(s(s(z))))=\lambda f.(\lambda sz.s(z))((\lambda z.f(f(f(z)))))=\lambda f.\lambda z.f(f(f(z)))=3}

La mwaq8logica booleana o algebra di Boole, è una formalizzazione della logica che si basa su due valori, cioè vero e falso, esprimibili come di seguito.

mware V := λ λ v f . v = λ λ v . λ λ f . v {\displaystyle V:=\lambda vf.v=\lambda v.\lambda f.v}

mwarm F := λ λ v f . f = λ λ v . λ λ f . f {\displaystyle F:=\lambda vf.f=\lambda v.\lambda f.f}

Da notarsi che la funzione mwaru F {\displaystyle F} rappresenta sia il valore zero che falso.

Di seguito, verranno espresse alcune delle più semplici operazioni relative alla logica booleana.

| Funzione Logica | Simbolo | Definizione |

|---|---|---|

| E (AND) | ∧ {\displaystyle \land } | λ p . λ p ′ . p p ′ p {\displaystyle \lambda p.\lambda p'.p\,p'p} |

| O (OR) | ∨ {\displaystyle \lor } | λ p . λ p ′ . p p p ′ {\displaystyle \lambda p.\lambda p'.p\,p\,p'} |

| NON (NOT) | ¬ {\displaystyle \neg } | λ p . p F V {\displaystyle \lambda p.p\,F\,V} |

mwati V A N D F = ( λ λ v f . v ) ( λ λ p p ′ . p p ′ p ) ( λ λ v f . f ) = ( λ λ v f . v ) ( λ λ v f . f ) ( λ λ v f . v ) = λ λ f . λ λ f . f = λ λ v f . f = F a l s o {\displaystyle V\;AND\;F=(\lambda vf.v)(\lambda pp'.p\,p'p)(\lambda vf.f)=(\lambda vf.v)(\lambda vf.f)(\lambda vf.v)=\lambda f.\lambda f.f=\lambda vf.f=Falso}

mwatq V O R V = ( λ λ v f . v ) ( λ λ p p ′ . p p p ′ ) ( λ λ v f . v ) = ( λ λ v f . v ) ( λ λ v f . v ) ( λ λ v f . v ) = λ λ v f . v = V e r o {\displaystyle V\;OR\;V=(\lambda vf.v)(\lambda pp'.p\,p\,p')(\lambda vf.v)=(\lambda vf.v)(\lambda vf.v)(\lambda vf.v)=\lambda vf.v=Vero}

mwaty N O T V = ( λ λ p . p ( λ λ v f . f ) ( λ λ v f . v ) ) ( λ λ v f . v ) = ( λ λ v f . v ) ( λ λ v f . f ) ( λ λ v f . v ) = ( λ λ f . λ λ v f . f ) ( λ λ v f . v ) = λ λ v f . f = F a l s o {\displaystyle NOT\;V=(\lambda p.p(\lambda vf.f)(\lambda vf.v))(\lambda vf.v)=(\lambda vf.v)(\lambda vf.f)(\lambda vf.v)=(\lambda f.\lambda vf.f)(\lambda vf.v)=\lambda vf.f=Falso}

Un termine del lambda calcolo si trova in mwatkforma normale se esso mwatonon è riscrivibile per mezzo della regola di beta riduzione. Se la beta riduzione rappresenta un passo di computazione di un lambda termine che descrive un programma, allora la sua mwatschiusura mwatwtransitiva ne rappresenta una qualsiasi computazione. Quando una riduzione è finita e mwat0massimale, il termine ridotto in forma normale rappresenta il risultato finale della computazione.

Per esempio, si supponga di arricchire il calcolo aggiungendovi i mwat8numeri naturali (semplicemente denotati come mwaua 1 , 2 , … … {\displaystyle 1,2,\ldots } ) e l'operazione di mwaueaddizione binaria su di essi (scritta in forma prefissa come mwaui ( + x y ) {\displaystyle (+xy)} ), entrambi peraltro direttamente codificabili come lambda termini. Si consideri ora un termine che somma mwaum 2 {\displaystyle 2} al suo argomento, ovvero mwauq ( λ λ x . ( ( + 2 x ) ) {\displaystyle (\lambda x.((+\ 2\ x))} e si usi come argomento il valore mwauu 5 {\displaystyle 5} . Tale applicazione converge a forma normale mwauy 7 {\displaystyle 7} , infatti: mwauc ( λ λ x . ( ( + 2 x ) ) 5 ) → → β β ( + 2 5 ) → → β β 7 ↛ β β {\displaystyle (\lambda x.((+\ 2\ x))5)\rightarrow _{\beta }(+\ 2\ 5)\rightarrow _{\beta }7\not \rightarrow _{\beta }} .

Non tutti i lambda termini hanno forma normale e la beta riduzione non ha sempre lunghezza finita. Questo fenomeno rappresenta il fatto che il calcolo di un programma può procedere indefinitamente e divergere e permette di rappresentare funzioni parziali.

L'esempio classico di divergenza è costruibile a partire dal termine duplicatore mwaus δ δ = d e f λ λ x . ( x x ) {\displaystyle \delta =_{def}\lambda x.(xx)} , che non fa altro che prendere un termine e restituirne due copie, l'una applicata all'altra. È possibile dunque definire il termine mwauw ω ω = d e f ( δ δ δ δ ) {\displaystyle \omega =_{def}(\delta \delta )} , e notare che esso riduce a se stesso mwau0 ω ω → → β β ω ω → → β β … … {\displaystyle \omega \rightarrow _{\beta }\omega \rightarrow _{\beta }\dots } .

cite-note-11. ↑ Barendregt, mwavqThe Lambda Calculus

• mwavg(EN) Henk P. Barendregt, mwavoThe Lambda Calculus, its Syntax and Semantics - Studies in Logic Volume 40, College Publication, London, 2012. ISBN 978-1-84890-066-0. Questo libro è una fonte enciclopedica per quanto riguarda il lambda calcolo non tipato. In esso sono presenti moltissime definizioni e dimostrazioni, ma pochissime spiegazioni sul significato e sull'interpretazione dei risultati presentati.

• Maurizio Gabbrielli e Simone Martini, mwav0Linguaggi di programmazione: principi e paradigmi, 2ª edizione, Milano, mwav4McGraw-Hill, 2011. ISBN 978-88-386-6573-8.

• mwawe(EN) Jean-Yves Girard, Proofs and Types, Paul Taylor and Yves Lafont, Cambridge University Press, 2003 [1989], ISBN 0-521-37181-3. URL consultato il 24 marzo 2014. Libro riguardante il lambda calcolo tipato e quello del secondo ordine.

• mwawuLambda calcolo di secondo ordine

• mwawcFunzione anonima

• mwawkProgrammazione funzionale

Altri progetti

• Wikimedia Commons

• Wikimedia Commons contiene immagini o altri file sul lambda calcolo

• citerefbritannica-com(EN) lambda calculus, su Enciclopedia Britannica, Encyclopædia Britannica, Inc.

• citerefinternet-encyclopedia-of-philosophy(EN) Shane Steinert-Threlkeld, Lambda Calculi, su Internet Encyclopedia of Philosophy.

• citerefstanford-encyclopedia-of-philosophy(EN) Alama, Jesse e Korbmacher, Johannes, The Lambda Calculus, su Stanford Encyclopedia of Philosophy, 12 dicembre 2012.

• citerefmathworld(EN) Eric W. Weisstein, Lambda Calculus, su MathWorld, Wolfram Research.

• citereffoldoc(EN) Denis Howe, lambda-calculus, in Free On-line Dictionary of Computing. Disponibile con licenza mwaxaGFDL

• (IT) Esempio di tesi su Lambda calcolomwaxi : "Compilatore Zmwaxm : XML tra Source e Target", su mwaxqtesionline